\begin{tabbing}
S\=ubst primrec(1+($n$ {-} 1);p{-}id();$\lambda$$i$,$g$. $f$ o $g$  ) = $f$ o primrec($n$ {-} 1;p{-}id();$\lambda$$i$,$g$. $f$ o $g$  )  \+
\\[0ex]0 THEN Auto
\-
\end{tabbing}